q(0(x1)) → p(p(s(s(0(s(s(s(s(x1)))))))))
q(s(x1)) → p(p(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))))
r(0(x1)) → p(s(p(s(0(p(p(p(s(s(s(x1)))))))))))
r(s(x1)) → p(s(p(s(s(q(p(s(p(s(x1))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(x1))))
↳ QTRS
↳ DependencyPairsProof
q(0(x1)) → p(p(s(s(0(s(s(s(s(x1)))))))))
q(s(x1)) → p(p(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))))
r(0(x1)) → p(s(p(s(0(p(p(p(s(s(s(x1)))))))))))
r(s(x1)) → p(s(p(s(s(q(p(s(p(s(x1))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(x1))))
Q(s(x1)) → P(s(s(x1)))
P(p(s(x1))) → P(x1)
R(0(x1)) → P(s(0(p(p(p(s(s(s(x1)))))))))
R(s(x1)) → P(s(x1))
R(s(x1)) → P(s(p(s(x1))))
Q(s(x1)) → P(p(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))))
R(0(x1)) → P(s(s(s(x1))))
Q(s(x1)) → R(p(p(s(s(x1)))))
Q(0(x1)) → P(p(s(s(0(s(s(s(s(x1)))))))))
Q(0(x1)) → P(s(s(0(s(s(s(s(x1))))))))
Q(s(x1)) → P(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))
R(0(x1)) → P(s(p(s(0(p(p(p(s(s(s(x1)))))))))))
R(0(x1)) → P(p(s(s(s(x1)))))
R(s(x1)) → P(s(p(s(s(q(p(s(p(s(x1))))))))))
Q(s(x1)) → P(p(s(s(x1))))
R(s(x1)) → Q(p(s(p(s(x1)))))
R(s(x1)) → P(s(s(q(p(s(p(s(x1))))))))
R(0(x1)) → P(p(p(s(s(s(x1))))))
q(0(x1)) → p(p(s(s(0(s(s(s(s(x1)))))))))
q(s(x1)) → p(p(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))))
r(0(x1)) → p(s(p(s(0(p(p(p(s(s(s(x1)))))))))))
r(s(x1)) → p(s(p(s(s(q(p(s(p(s(x1))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(x1))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q(s(x1)) → P(s(s(x1)))
P(p(s(x1))) → P(x1)
R(0(x1)) → P(s(0(p(p(p(s(s(s(x1)))))))))
R(s(x1)) → P(s(x1))
R(s(x1)) → P(s(p(s(x1))))
Q(s(x1)) → P(p(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))))
R(0(x1)) → P(s(s(s(x1))))
Q(s(x1)) → R(p(p(s(s(x1)))))
Q(0(x1)) → P(p(s(s(0(s(s(s(s(x1)))))))))
Q(0(x1)) → P(s(s(0(s(s(s(s(x1))))))))
Q(s(x1)) → P(s(s(s(s(s(s(r(p(p(s(s(x1))))))))))))
R(0(x1)) → P(s(p(s(0(p(p(p(s(s(s(x1)))))))))))
R(0(x1)) → P(p(s(s(s(x1)))))
R(s(x1)) → P(s(p(s(s(q(p(s(p(s(x1))))))))))
Q(s(x1)) → P(p(s(s(x1))))
R(s(x1)) → Q(p(s(p(s(x1)))))
R(s(x1)) → P(s(s(q(p(s(p(s(x1))))))))
R(0(x1)) → P(p(p(s(s(s(x1))))))
q(0(x1)) → p(p(s(s(0(s(s(s(s(x1)))))))))
q(s(x1)) → p(p(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))))
r(0(x1)) → p(s(p(s(0(p(p(p(s(s(s(x1)))))))))))
r(s(x1)) → p(s(p(s(s(q(p(s(p(s(x1))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(x1))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
P(p(s(x1))) → P(x1)
q(0(x1)) → p(p(s(s(0(s(s(s(s(x1)))))))))
q(s(x1)) → p(p(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))))
r(0(x1)) → p(s(p(s(0(p(p(p(s(s(s(x1)))))))))))
r(s(x1)) → p(s(p(s(s(q(p(s(p(s(x1))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(x1))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P(p(s(x1))) → P(x1)
The value of delta used in the strict ordering is 1/32.
POL(P(x1)) = (1/2)x_1
POL(p(x1)) = (1/4)x_1
POL(s(x1)) = 1/4 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
q(0(x1)) → p(p(s(s(0(s(s(s(s(x1)))))))))
q(s(x1)) → p(p(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))))
r(0(x1)) → p(s(p(s(0(p(p(p(s(s(s(x1)))))))))))
r(s(x1)) → p(s(p(s(s(q(p(s(p(s(x1))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(x1))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
R(s(x1)) → Q(p(s(p(s(x1)))))
Q(s(x1)) → R(p(p(s(s(x1)))))
q(0(x1)) → p(p(s(s(0(s(s(s(s(x1)))))))))
q(s(x1)) → p(p(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))))
r(0(x1)) → p(s(p(s(0(p(p(p(s(s(s(x1)))))))))))
r(s(x1)) → p(s(p(s(s(q(p(s(p(s(x1))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(x1))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
R(s(x1)) → Q(p(s(p(s(x1)))))
Used ordering: Polynomial interpretation [25,35]:
Q(s(x1)) → R(p(p(s(s(x1)))))
The value of delta used in the strict ordering is 1/2.
POL(Q(x1)) = 1/2 + (4)x_1
POL(s(x1)) = 4 + (2)x_1
POL(p(x1)) = 1/4 + (1/2)x_1
POL(0(x1)) = 1/2
POL(R(x1)) = 3 + (4)x_1
p(p(s(x1))) → p(x1)
p(0(x1)) → 0(s(s(s(x1))))
p(s(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
Q(s(x1)) → R(p(p(s(s(x1)))))
q(0(x1)) → p(p(s(s(0(s(s(s(s(x1)))))))))
q(s(x1)) → p(p(s(s(s(s(s(s(r(p(p(s(s(x1)))))))))))))
r(0(x1)) → p(s(p(s(0(p(p(p(s(s(s(x1)))))))))))
r(s(x1)) → p(s(p(s(s(q(p(s(p(s(x1))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(x1))))